i, x:Id, k:Knd, ds:x:Id fp Type, da:a:Knd fp Type, f:(State(ds)Valtype(da;k)ds(x)?Void).
@i: with declarations ds:dsda:daeffect of k(v) is x := f s v  Dsys 

latex

Definitions	Dsys, @i: with declarations ds:dsda:daeffect of k(v) is x := f s v, if b then t else f fi , f(a), eqof(d), MsgA, with declarations ds:dsda:daeffect of k(v) is x := f s v, , State(ds), Valtype(da;k), x:AB(x), , f(x)?z, x.A(x), IdDeq, Void, a:A fp B(a), x:A. B(x), x. t(x), Type, Knd, t  T, Id
Lemmas	Id wf, Knd wf, fpf wf, id-deq wf, fpf-cap wf, rationals wf, ma-valtype wf, ma-state wf, ma-empty wf, ma-single-effect wf, msga wf, eqof wf, ifthenelse wf